Inference at * 
Iof proof for Lemma do-apply-p-lift:


  A, B:Type, P:(A), d:(x:ADec(P(x))), f:({x:A| P(x)} B), x:A.
  (can-apply(p-lift(d;f);x))  (do-apply(p-lift(d;f);x) = f(x)) 

latex

 by ((((Auto) 
CollapseTHEN (MoveToConcl (-1)))) 
CollapseTHEN (RepUR ``
Ccan-apply do-apply p-lift`` ( 0))) 

latex

C1: 

C1: 1. A : Type
C1: 2. B : Type
C1: 3. P : A
C1: 4. d : x:ADec(P(x))
C1: 5. f : {x:A| P(x)} B
C1: 6. x : A
C1:   (isl(case d(x) of inl(a) => inl (f(x))  | inr(a) => inr a ))
C1:    (outl(case d(x) of inl(a) => inl (f(x))  | inr(a) => inr a ) = f(x))
C.

Definitions	x. t(x), x.A(x), suptype(S; T), S  T, Top, x:A.B(x), Void, {x:A| B(x)} , x:A. B(x), Dec(P), x(s), f(a), , s = t, t  T, Type, P  Q, x:AB(x), can-apply(f;x), p-lift(d;f), do-apply(f;x), b
Lemmas	assert wf, can-apply wf, p-lift wf, top wf, member wf, decidable wf